es:ES, d, b, a, c:E. a  b   c  d   [a, b] = [c, d]  E List  {a = c & b = d} 

latex

Definitions	x:A. B(x), P  Q, t  T, Prop, ij, T, True, P  Q, P  Q, P & Q, {T}, SqStable(P)
Lemmas	es-E wf, es-interval wf, es-le wf, event system wf, hd-es-interval, hd wf, sq stable from decidable, le wf, length wf1, decidable le, ge wf, pos length, not functionality wrt iff, es-locl wf, es-interval-nil, es-le-loc, es-loc wf, squash wf, true wf, es-le-not-locl, es-interval-length-one-one